i:Id, M:MsgA. Feasible(M)  Feasible((@i M)) 

latex

Definitions

t  T, P & Q, Feasible(D), P  Q, x:A. B(x), Prop, false, true, if b t else f fi, (@i M), M(i), P  Q, P  Q, 2of(t), 1of(t), M.din(l,tg), M.dout(l,tg), x. t(x), Y, reduce(f;k;as), deq-member(eq;x;L), x  dom(f), Top, , mk-ma, f(x)?z, , x:A. B(x), map(f;as), M sends on link l, b, Unit, , Valtype(da;k), MsgA, x(s), f(x), A & B, a:A fp B(a), False,

Lemmas

Id wf, msga wf, ma-feasible wf, ma-empty-feasible, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, id-deq wf, eqof wf, IdLnk wf, lsrc wf, ldst wf, deq property, rcv wf, Kind-deq wf, Knd wf, subtype-fpf-cap-top, fpf-sub-reflexive, top wf, ma-dout wf, ifthenelse wf, ma-din wf, ma-empty wf, decidable assert, decidable equal Id, decidable cand, ma-sends-on wf, finite-decidable-set, pi2 wf, map wf, false wf, idlnk-deq wf, deq-member wf, assert-deq-member, fpf-cap wf, ma-state wf, l member wf, pi1 wf